COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	declare INDVAR t t1 t2 t3 t4 ε tower
C00005 ENDMK
C⊗;
declare INDVAR t t1 t2 t3 t4 ε tower;
declare INDVAR s s0 s1 s2 s3 ε situation;

declare PREDCONST movable(tower,tower,situation),on(tower,tower,situation);
declare PREDCONST moves(tower,tower,situation,situation);
declare PREDCONST reachable(situation,situation);
declare OPCONST move(tower,tower,situation) = situation;
declare OPCONST movefromto(tower,tower,situation);
declare PREDPAR P 1;

axiom move:
	∀t1 t2 s.(movable(t1,t2,s) ⊃ on(t1,t2,move(t1,t2,s))
		∧ ∀t3 t4.(¬(t3=t1) ⊃ (on(t3,t4,move(t1,t2,s)) ≡ on(t3,t4,s))))
	∀t1 t2 s.(¬movable(t1,t2,s) ⊃ move(t1,t2,s) = s)

	∀t1 t2 s.(movable(t1,t2,s) ⊃ ∃s1.(reachable(s,s1) ∧
		on(t1,t2,s1) ∧ ∀t3 t4.(¬(t3=t1) ⊃ (on(t3,t4,s1) ≡ on(t3,t4,s)))))
;;

axiom reachable:
	∀t1 t2 s.(movable(t1,t2,s) ⊃ reachable(s,move(t1,t2,s)))
	∀s.reachable(s,s)
	∀s1 s2 s3.(reachable(s1,s2) ∧ reachable(s2,s3) ⊃ reachable(s1,s3))
	∀s1 s2 t1 t2.(reachable(s1,s2) ∧movable(t1,t2,s2) ⊃
				reachable(s1,move(t1,t2,s2)))
	∀s0.(P(s0) ∧ ∀s t1 t2.(P(s) ∧ movable(t1,t2,s) ⊃ P(move(t1,t2,s)))
				⊃ ∀s.(reachable(s0,s) ⊃ P(s)))
;;

axiom movefromto:
	∀t1 t2 s.(∃t4.(on(t4,t1,s) ∧ movable(t4,t2,s)) ⊃
		∃t3.moves(t3,t2,s,movefromto(t1,t2,s)))
;;

axiom moves:
	∀t1 t2 s1 s2.(moves(t1,t2,s1,s2) ⊃ on(t1,t2,s2) ∧
		∀t.(¬(t=t1) ⊃ (on(t,t3,s2) ≡ on(t,t3,s1))))
;;